T:Type, P:(TProp).
(x:T. Dec(P(x)))  (finite-type({x:T| P(x) })  (L:T List. x:T. P(x)  (x  L))) 

latex

Definitions	filter(P;l), True, False, true, false, P  Q, A, , b, Dec(P), x. t(x), finite-type(T), t  T, SqStable(P), Prop, P & Q, P  Q, P  Q, x:A. B(x), x:A. B(x), P  Q, (x  l), x(s)
Lemmas	l member wf, sq stable from decidable, iff wf, finite-type wf, finite-set-type, iff functionality wrt iff, decidable wf, assert wf, bfalse wf, btrue wf, not wf, false wf, true wf, member filter, all functionality wrt iff, filter wf